Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	minus(minus(x))	→ x
2:	minus(x + y)	→ minus(minus(minus(x))) * minus(minus(minus(y)))
3:	minus(x * y)	→ minus(minus(minus(x))) + minus(minus(minus(y)))
4:	f(minus(x))	→ minus(minus(minus(f(x))))

There are 16 dependency pairs:

The approximated dependency graph contains 2 SCCs: {5-16} and {20}.

Consider the SCC {5-16}. The usable rules are {1-3}. The constraints could not be solved.

Consider the SCC {20}. There are no usable rules. By taking the AF π with π(F) = 1 together with the lexicographic path order with empty precedence, rule 20 is strictly decreasing.

Tyrolean Termination Tool (0.40 seconds) --- May 3, 2006